state@$i$$\backslash\backslash$$x$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$y$:Id$\rightarrow$if $y$ = $x$$\rightarrow$ Top else vartype($i$;$y$) fi